x, y:Atom1. x =a1 y  x = y 

latex

Definitions	t  T, Atom$n, Type, s = t, Prop, b, x:A. B(x), eq_atom$n(x;y), P  Q, P  Q, P & Q, P  Q, left+right, P  Q, Dec(P), b, , false, False, A, x:AB(x), x:AB(x), true
Lemmas	eqtt to assert, btrue wf, assert of bnot, bfalse wf, eqff to assert, decidable atom equal 1, assert wf, eq atom wf1